Nuprl Definition : p-compose'
11,40
postcript
pdf
f
o'
g
(
x
) == if can-apply(
g
;
x
) then inl (
f
(
x
,do-apply(
g
;
x
))) else
g
(
x
) fi
latex
Definitions
x
.
A
(
x
)
,
if
b
then
t
else
f
fi
,
can-apply(
f
;
x
)
,
inl
x
,
do-apply(
f
;
x
)
,
f
(
a
)
FDL editor aliases
p-compose'
origin
x.A(x)x.A(x)